The present disclosure relates generally to a verified inference engine for autonomous control of a system.
An inference engine is an artificial intelligence program that reasons about a set of rules in a rule base and fires rules based on information stored in a fact base. The fact base is a list of known facts that the inference engine stores. The inference engine can perform this reasoning with a forward-chaining or backward-chaining approach. The inference engine can fire the rules that it reasons about to create outputs for the inference engine as well as new information to be stored in the fact base.
One use of an inference engine is in an autonomous vehicle. Autonomous vehicles include a plurality of vehicle types. Autonomous vehicles include but are not limited to autonomous commercial aircraft, autonomous military aircraft, self-driving cars, autonomous surface ships, autonomous underwater vehicles (AUVs) and spacecraft. For many of these vehicles, high assurance of the inference engine design and operation is needed to verify that the autonomous control of the vehicle exhibits a high degree of reliability.
When an inference engine is used in an autonomous vehicle, a fact base may include information regarding the surroundings of the vehicle such as terrain, weather conditions, other vehicles, the physical surroundings of the autonomous vehicle, vehicle latitude/longitude, altitude/depth, speed, acceleration, pitch, roll, and yaw. The rule base applies a set of rules to the fact base and creates system outputs as well new facts for the fact base. The inference engine learns new facts and stores them in the fact base for future use in determining control outputs for the autonomous vehicle.
When an inference engine is used in an autonomous vehicle, it must meet a high degree of assurance. In aviation, the highest level of design assurance prevents failures which may cause the autonomous vehicle to suffer a catastrophic failure. A system in which a failure can be catastrophic needs to meet the highest level of design assurance. Details regarding the assurance levels necessary to control a vehicle with an inference engine can be found in development standards such as RTCA DO-178C, Software Considerations in Airborne Systems and Equipment Certification, Level A (for safe operation); and Evaluation Assurance Level 7 (EAL-7) of the Common Criteria (for secure operation). A Level A failure condition in the DO-178C standard is labeled catastrophic. To verify that software meets the DO-178C Level A standard, the software is tested with the modified condition/decision coverage (MC/DC) criterion. MC/DC coverage states four criteria for software. One criterion is that each entry and exit point is invoked. A second criterion is that each decision takes every possible outcome. A third criterion is that each condition in a decision takes every possible outcome. A fourth criterion is that each condition in a decision is shown to independently affect the outcome of the decision.
Inference engines used in autonomous vehicles must meet reliability standards such as the DO-178C Level A standard, or EAL-7 of the Common Criteria. To implement high assurance in an inference engine, a rule validator can be used to assure that the rules designed for the rule base are valid and consistent. Consistency in the rules stored in the rule validator leads to an inference engine that does not execute contradictory commands.
Further, high assurance can be achieved by validation of inputs and outputs of the inference engine. Validating all inputs from input sources provides the inference engine with reliable input data and stops the inference engine from making decisions based on flawed or unreliable data and verifies that the inference engine makes decisions based on reliable data. Validating the outputs of the inference engine verify that the autonomous vehicle will not be commanded to perform any forbidden maneuvers. Forbidden maneuvers may be maneuvers that may cause the autonomous vehicle to lose control or crash, stray into controlled airspace, etc.
Further, a method for verifying an inference engine can be implemented using an automated theorem proving tool. Automated theorem proving tools can be used to prove the mathematical correctness of the inference engine design and implementation.